The main usage of command line is of the following format:

PAT.Console.exe [module] [options]* inputFile outputFile

for example: PAT.Console.exe -csp -sp DiningPhilosopher.csp result.txt .

For [module] part, the paragraph below lists all the supported commands corresponding to different modules:

• -csp: Verification using CSP Module. If there is no module option is given, this is the default one.
• -rts: Verification using Real-Time System Module.
• -pcsp: Verification using Probabilistic CSP Module.
• -prts: Verification using Probabilistic Real-Time System Module.
• -module short name: Put the short name of your module, which should be the folder name of your module. 

For [options] part, here is the list for all the choices:

• -b: (B)atch mode, the inputFile will be the batch file containing lines of examples.
              Each line shall have the following format: -f inputFile
• -d: (D)irectory mode, the inputFile shall be the input directory name. All examples inside the directory will be executed.
              Please use only -b or -d
• -behavior n: specify the admissible behavior as integer value n. Default value is 0.
• -engine n: specify the search engine as integer value n. Default value is 0.
• -help: print HELP information.
• -nc: (N)o (C)ounterexample display.
• -on: (O)n-the-fly Normalization. Suggest not to use, since static normalization is usually faster.
• -v: (V)erbose mode.
• -ver: (VER)sion.

The UML related of command line usage is of the following two formats:

                                PAT.Console.exe -uml inputFile outputFile

The command firstly translates inputFile into a CSP# model and outputs the CSP# model to outputFile.

                          PAT.Console.exe -uml inputFile1 inputFile2 outputFile

The command firstly translates inputFile1 and inputFile2 into two CSP# models respectively, say input1 and input2, then verifies whether input1 refines input2 in the trace semantics, i.e. the assertion "#assert input1 refines input2", and outputs the result to outputFile.